n:, q:. 0  i < n. q = (n * q)   

latex

Definitions	T, True, , P & Q, x. t(x), P  Q, P  Q, False, A, A  B, i  j , P  Q, t  T, x:A. B(x), x(s), , S  T
Lemmas	qmul one qrng, true wf, squash wf, qmul over plus qrng, qadd-add, qadd wf, sum unroll hi q, qmul zero qrng, sum unroll base q, int inc rationals, qmul wf, int seg wf, rationals wf, ge wf, nat properties, nat wf